\begin{tabbing}
ecl{-}mng\=\{i:l\}\+
\\[0ex](${\it es}$; $i$; ${\it ds}$; ${\it da}$; $x$; ${\it snd}$; ${\it upd}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$l$$\in$msg{-}spec{-}links(${\it snd}$).ecl{-}mng{-}sends\{i:l\}(${\it es}$; $i$; ${\it ds}$; ${\it da}$; $x$; $l$; ${\it snd}$)\+
\\[0ex]\& $\forall$$z$$\in$update{-}spec{-}vars(${\it upd}$).ecl{-}mng{-}update\{i:l\}(${\it es}$; $i$; ${\it ds}$; ${\it da}$; $x$; $z$; ${\it upd}$)
\-
\end{tabbing}